Inference at * 2 2 1 
Iof proof for Lemma member-zip:



1. A : Type
2. B : Type
3. A List
4. u : A
5. v : A List
6. ys:(B List), x:A, y:B. (<x, y>  zip(v;ys))  {(x  v) & (y  ys)}
7. B List
8. u1 : B
9. v1 : B List
10. x:A, y:B. (<x, y>  zip([u / v];v1))  {(x  [u / v]) & (y  v1)}
11. x : A
12. y : B
13. <x, y> = <u, u1>
  {(x  [u / v]) & (y  [u1 / v1])} 

latex

 by EqHD (-1) THEN All Reduce THEN Auto 
THEN Unfold `guard` 0 THEN RWO "cons_member" 0 THEN Auto 

THTHEN OrLeft THEN Auto 

latex

TH.

Definitions	t.2, t.1, x. t(x), x.A(x), {T}, P  Q, x:A  B(x), P  Q, P  Q, x:AB(x), [car / cdr], , P & Q, left + right, s = t, P  Q, (x  l), x:A. B(x), t  T
Lemmas	pi2 wf, pi1 wf, and functionality wrt iff, cons member, l member wf